\begin{tabbing}
$\forall$\=${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $v$:ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$),\+
\\[0ex]$z$:ecl{-}trans{-}type($v$), $L$:(event{-}info(${\it ds}$;${\it da}$) List).
\-\\[0ex]ecl{-}trans{-}state{-}from($v$; $z$; $L$) $\in$ ecl{-}trans{-}type($v$)
\end{tabbing}